\begin{tabbing}
$\vdash$  \=$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$), $f$:($\forall$$x$:$T$. Dec($P$($x$))), $x$:$T$.\+
\\[0ex]($\uparrow$can{-}apply(p{-}filter($f$);$x$)) $\Rightarrow$ (do{-}apply(p{-}filter($f$);$x$) = $x$)
\-
\end{tabbing}